es:ES, x, free:Id, n:, e:E.
@loc(e)(x:Id)
 (((x after e) = (x when e)  Id))
 <n, 0> < rank(e)
 (e':E
 ((e' loc e 
 (& rank(e') = <n, 1>  (:  )
 (& (((x after e') = (x when e')  Id))
 (& ((x changed before e')  ((x when e') = free)))) 

latex

Definitions

{T}, x < y, inc-snd(p), True, T, inc-fst(p), let x = a in b(x), ff, tt, if b then t else f fi , Y, rank(e), False, P  Q, A c B, A  B, S  T, x. t(x), , t  T, (e <loc e'), e loc e' , P & Q, x:A. B(x), A, @i(x:T), P  Q, , x:A. B(x), @e(xv), t.2, t.1, P  Q, Unit, , Dec(P), x(s), WellFnd{i}(A;x,y.R(x;y)),

Lemmas

es-le weakening, es-locl transitivity1, es-le wf, decidable lt, change-to-last-change, decidable assert, es-when-first-discrete, last-change-property, inc-fst wf, inc-snd wf, pi2 wf, pi1 wf, loc-last-change, last-change wf, not functionality wrt iff, assert-eq-id, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bnot wf, bool wf, id-deq wf, es-le weakening eq, decidable equal nat, decidable equal product, event system wf, Id wf, le wf, es-causl wf, nat wf, es-loc wf, changed wf, es-dtype wf, es-le-loc, es-locl wf, f-rank wf, intpair-less wf, es-when wf, es-after wf, not wf, es-vartype wf, es-isconst wf, assert wf, es-locl-wellfnd